FDL - Step of Proof: p-compose-associative

Step of Proof: p-compose-associative

11,40

Inference at *
Iof proof for Lemma p-compose-associative:

A, B, C, D:Type, h:(A

(B + Top)), g:(B

(C + Top)), f:(C

(D + Top)).

f o g o h = f o g o h

by ((Auto

)

CollapseTHEN (((Ext)

CollapseTHEN (((Auto

)

CollapseTHEN (((RepUR ``

Cp-compose can-apply do-apply`` ( 0)

)

CollapseTHEN ((if (((first_nat 2:n)) = 0) then (Repeat (((

C((GenConclAtAddr [3;1;1])
CollapseTHENA (Auto

))

)
CCollapseTHEN (((D (-2)

)
CCollapseTHEN (((
CCReduce 0)
CCollapseTHEN ((Try ((Complete (Auto

))

)) else (RepeatFor (first_nat 2:n
CC) (((((GenConclAtAddr [3;1;1])
CollapseTHENA (Auto

))

)
CCollapseTHEN (((D (-2)

)

CCoCollapseTHEN (((Reduce 0)
CCollapseTHEN ((Try ((Complete (Auto

))

)))

))

))
CC

CC.

Definitions can-apply(f;x), do-apply(f;x), if b then t else f fi , isl(x), outl(x), b, S T, P Q, f(a), inl x , Top, inr x , Decision, left + right, Type, f o g , x:A. B(x), x:AB(x), t T, s = t

Lemmas ifthenelse wf, isl wf, outl wf, assert wf, member wf, top wf, p-compose wf

Definitions	can-apply(f;x), do-apply(f;x), if b then t else f fi , isl(x), outl(x), b, S T, P Q, f(a), inl x , Top, inr x , Decision, left + right, Type, f o g , x:A. B(x), x:AB(x), t T, s = t
Lemmas	ifthenelse wf, isl wf, outl wf, assert wf, member wf, top wf, p-compose wf